Library TrianglesDefs
Require Export PointsETC.
Require Import ConwayNotations.
Require Import incidence.
Definition cevian_triangle P :=
match P with cTriple p q r ⇒
(cTriple 0 q r, cTriple p 0 r, cTriple p q 0)
end.
Definition anti_cevian_triangle P :=
match P with cTriple p q r ⇒
(cTriple (-p) q r, cTriple p (-q) r, cTriple p q (-r))
end.
Section Triangle.
Context `{M:triangle_theory}.
Definition pedal_triangle P :=
match P with cTriple p q r ⇒
(cTriple 0 (q+p*(-a^2-b^2+c^2)/(-2×a×b)) (r + p*(-a^2+b^2-c^2)/(-2×a×c)),
cTriple (p + q*(-a^2-b^2+c^2)/(-2×a×b)) 0 (r+q*(a^2-b^2-c^2)/(-2×b×c)),
cTriple (p + r*(-a^2+b^2-c^2)/(-2×a×c)) (q+r*(a^2-b^2-c^2)/(-2×b×c)) 0)
end.
Definition incentral_triangle := cevian_triangle X_1.
Definition medial_triangle := cevian_triangle X_2.
Definition orthic_triangle := cevian_triangle X_4.
Definition intouch_triangle := cevian_triangle X_7.
Definition extouch_triangle := cevian_triangle X_8.
Lemma cevian_triangle_ok :
∀ P,
match cevian_triangle P with
(X,Y,Z) ⇒ col pointA P X ∧ col pointB P Y ∧ col pointC P Z ∧
col X pointB pointC ∧ col Y pointA pointC ∧ col Z pointA pointB
end.
Proof.
intros.
destruct P.
unfold col;simpl.
repeat split;ring.
Qed.
Require Import ConwayNotations.
Require Import incidence.
Definition cevian_triangle P :=
match P with cTriple p q r ⇒
(cTriple 0 q r, cTriple p 0 r, cTriple p q 0)
end.
Definition anti_cevian_triangle P :=
match P with cTriple p q r ⇒
(cTriple (-p) q r, cTriple p (-q) r, cTriple p q (-r))
end.
Section Triangle.
Context `{M:triangle_theory}.
Definition pedal_triangle P :=
match P with cTriple p q r ⇒
(cTriple 0 (q+p*(-a^2-b^2+c^2)/(-2×a×b)) (r + p*(-a^2+b^2-c^2)/(-2×a×c)),
cTriple (p + q*(-a^2-b^2+c^2)/(-2×a×b)) 0 (r+q*(a^2-b^2-c^2)/(-2×b×c)),
cTriple (p + r*(-a^2+b^2-c^2)/(-2×a×c)) (q+r*(a^2-b^2-c^2)/(-2×b×c)) 0)
end.
Definition incentral_triangle := cevian_triangle X_1.
Definition medial_triangle := cevian_triangle X_2.
Definition orthic_triangle := cevian_triangle X_4.
Definition intouch_triangle := cevian_triangle X_7.
Definition extouch_triangle := cevian_triangle X_8.
Lemma cevian_triangle_ok :
∀ P,
match cevian_triangle P with
(X,Y,Z) ⇒ col pointA P X ∧ col pointB P Y ∧ col pointC P Z ∧
col X pointB pointC ∧ col Y pointA pointC ∧ col Z pointA pointB
end.
Proof.
intros.
destruct P.
unfold col;simpl.
repeat split;ring.
Qed.
The Cevian triangle of P wrt some triangle ABC
Definition cevian_triangle_gen P A B C :=
((inter (line A P) (line B C)),
(inter (line B P) (line A C)),
(inter (line C P) (line A B))).
Lemma cevian_triangle_cevian_triangle_gen : ∀ P,
eq_triangles (cevian_triangle P) (cevian_triangle_gen P pointA pointB pointC).
Proof.
intros.
destruct P.
simpl.
unfold eq_points;repeat split;simpl;ring.
Qed.
Lemma cevian_triangle_gen_ok :
∀ P A B C,
match cevian_triangle_gen P A B C with
(X,Y,Z) ⇒ col A P X ∧ col B P Y ∧ col C P Z ∧
col X B C ∧ col Y A C ∧ col Z A B
end.
Proof.
intros.
destruct P.
destruct A.
destruct B.
destruct C.
simpl.
unfold inter,line,col;simpl.
repeat split;ring.
Qed.
Lemma cevian_triangle_perspector : ∀ A B C P,
is_perspector P (cevian_triangle_gen P A B C) (A,B,C).
Proof.
intros.
destruct A;destruct B;destruct C;destruct P.
red;simpl;unfold col;simpl.
repeat split;ring.
Qed.
End Triangle.